es:ES, e:E, l:IdLnk, tg:Id.
(e sends on l with tag tg)  (sender(es-first-from(es;e;l;tg)) = e) 

latex

Definitions	Top, null(as), t.2, if b then t else f fi , tt, tag(k), b, outl(x), t.1, SQType(T), {T}, lnk(k), rcv(l,tg), hd(l), True, T, xL. P(x), x. t(x), , P & Q, A c B, t  T, es-first-from(es;e;l;tg), P  Q, IdLnk, x:A. B(x), False, A, P  Q, x:A. B(x), (e sends on l with tag tg), SqStable(P), P  Q, x(s), lnk(e), isrcv(e)
Lemmas	top wf, subtype rel list, null wf3, filter wf, member null, l member set, assert-eq-id, Knd wf, Knd sq, es-kind-rcv, member filter, decidable assert, isrcv wf, sq stable from decidable, tagof wf, eq id wf, es-kind wf, es-isrcv wf, assert wf, filter type, l member wf, member-es-receives, es-receives wf, list-set-type2, event system wf, es-E wf, IdLnk wf, Id wf, es-sends-on wf, es-sender wf, lnk wf